Example 24 in [Giesl and Middeldorp - JFP'04]

Summary: Ex24_GM04

• CS-TRS format
• OBJ format
• Negative results:
  1. Lucas' transformation (non-terminating)
  2. Zantema's transformation (non-terminating)
  3. Ferreira and Ribeiro's transformation (non-terminating)
  4. Giesl and Middeldorp's transformation (non-terminating)
  5. CSRPO
• Positive results:
  1. Polynomial interpretation
  2. CSDP

CS-TRS Ex24_GM04 (file Ex24_GM04.csr)

Functions:  f g b c

Constructors:  c

Variables:  X Y

Arities: 

ar(f) = 3
ar(g) = 1
ar(b) = 0
ar(c) = 0

Replacement map: 

µ(f)={}
µ(g)={1}
µ(b)={}
µ(c)={}

Rules: (file Ex24_GM04)  

f(X,g(X),Y) -> f(Y,Y,Y)
g(b) -> c
b -> c

The CS-TRS in OBJ format (file Ex24_GM04.obj):

obj Ex24_GM04 is
  sort S .
  op f : S S S -> S [strat (0)] .
  op g : S -> S .
  op b : -> S .
  op c : -> S .
  vars X Y : S .
  eq f(X,g(X),Y) = f(Y,Y,Y) .
  eq g(b) = c .
  eq b = c .
endo

Negative results

1. The µ-termination of Ex24_GM04 cannot be proved by using Lucas' transformation. The TRS Ex24_GM04_L:

       f -> f
       g(b) -> c
       b -> c
       

   is not terminating.
2. The µ-termination of Ex24_GM04 cannot be proved by using Zantema's transformation. The TRS Ex24_GM04_Z:

       f(X,n__g(X),Y) -> f(activate(Y),activate(Y),activate(Y))
       g(b) -> c
       b -> c
       g(X) -> n__g(X)
       activate(n__g(X)) -> g(X)
       activate(X) -> X
       

   is not terminating:

       f(c,n__g(c),n__g(b)) 
          -> f(activate(n__g(b)),activate(n__g(b)),activate(n__g(b)))
          -> f(g(b),activate(n__g(b)),activate(n__g(b)))
          -> f(c,activate(n__g(b)),activate(n__g(b)))
          -> f(c,g(b),activate(n__g(b)))
          -> f(c,g(c),activate(n__g(b)))
          -> f(c,n__g(c),activate(n__g(b)))
          -> f(c,n__g(c),n__g(b))
          -> ... 
        

3. The µ-termination of Ex24_GM04 cannot be proved by using Ferreira and Ribeiro's transformation. The TRS Ex24_GM04_FR:

        f(X,n__g(X),Y) -> f(activate(Y),activate(Y),activate(Y))
        g(b) -> c
        b -> c
        g(X) -> n__g(X)
        activate(n__g(X)) -> g(activate(X))
        activate(X) -> X
        

   is not terminating:

        f(c,n__g(c),n__g(b)) 
   	-> f(activate(n__g(b)),activate(n__g(b)),activate(n__g(b)))
   	-> f(g(b),activate(n__g(b)),activate(n__g(b)))
   	-> f(c,activate(n__g(b)),activate(n__g(b)))
   	-> f(c,g(b),activate(n__g(b)))
   	-> f(c,g(c),activate(n__g(b)))
   	-> f(c,n__g(c),activate(n__g(b)))
   	-> f(c,n__g(c),n__g(b))
   	-> ... 
         

4. The µ-termination of Ex24_GM04 cannot be proved by using Giesl and Middeldorp's transformation. The TRS Ex24_GM04_GM:

        a__f(X,g(X),Y) -> a__f(Y,Y,Y)
        a__g(b) -> c
        a__b -> c
        mark(f(X1,X2,X3)) -> a__f(X1,X2,X3)
        mark(g(X)) -> a__g(mark(X))
        mark(b) -> a__b
        mark(c) -> c
        a__f(X1,X2,X3) -> f(X1,X2,X3)
        a__g(X) -> g(X)
        a__b -> b
        

   is not terminating:

          a__f(c,g(c),a__g(a__b)) -> a__f(a__g(a__b),a__g(a__b),a__g(a__b))
   	  -> a__f(a__c,a__g(a__b),a__g(a__b))
   	  -> a__f(c,a__g(a__b),a__g(a__b))
   	  -> a__f(c,g(a__b),a__g(a__b))
   	  -> a__f(c,g(a__c),a__g(a__b))
   	  -> a__f(c,g(c),a__g(a__b))
   	  -> ...
       

5. No proof is possible by using CSRPO.

Positive results

1. The µ-termination of Ex24_GM04 is proved in [Luc04, Example 12] by using a polynomial interpretation:

      [f](x,y,z) = x^2 - 2xy + y^2 + z
      [g](x) = x + 1
      [b] = 1
      [c] = 0
      

2. The µ-termination of Ex24_GM04 can be proved by using CSDP (computed by MuTerm).